Nuprl Lemma : action_p_wf
13,42
postcript
pdf
A
:Type,
x
:(
A
A
A
),
e
:
A
,
S
:Type,
f
:(
A
S
S
). IsAction(
A
;
x
;
e
;
S
;
f
)
latex
Up
gen
algebra
1
Definitions of Statement
IsAction(
A
;
x
;
e
;
S
;
f
)
Definitions
x
f
y
,
P
&
Q
,
IsAction(
A
;
x
;
e
;
S
;
f
)
,
,
t
T
,
x
:
A
.
B
(
x
)
origin
A:Type, x:(A
AA), e:A, S:Type, f:(ASS). IsAction(A;x;e;S;f) 
A:Type, x:(AAA), e:A, S:Type, f:(ASS). IsAction(A;x;e;S;f) Tx:A. B(x)